T:(IdType), tab:secret-table(T), k1, k2:+Atom1. st-key-match(tab;k1;k2)   

latex

Definitions	false, t  T, , {x:A| B(x) }, x:AB(x), x:A. B(x), a<b, #$n, AB, x:AB(x), P & Q, i  j < k, {i..j}, st-atom(tab;n), eq_atom$n(x;y), , Type, Prop, True, ij, b, b, s = t, P  Q, T, P  Q, P  Q, Unit, left+right, False, A, , Void, p  q, st-key-match(tab;k1;k2), Id, secret-table(T), Atom$n, ||tab|| , i<j, ptr(tab)
Lemmas	secret-table wf, Id wf, st-ptr wf, band wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, bnot wf, assert wf, le int wf, lt int wf, bool wf, eq atom wf1, st-atom wf, le wf, st-length wf, nat wf, bfalse wf